Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		not(x)	→ xor(x,true)
2:		or(x,y)	→ xor(and(x,y),xor(x,y))
3:		implies(x,y)	→ xor(and(x,y),xor(x,true))
4:		and(x,true)	→ x
5:		and(x,false)	→ false
6:		and(x,x)	→ x
7:		xor(x,false)	→ x
8:		xor(x,x)	→ false
9:		and(xor(x,y),z)	→ xor(and(x,z),and(y,z))

There are 10 dependency pairs:


10:		NOT(x)	→ XOR(x,true)
11:		OR(x,y)	→ XOR(and(x,y),xor(x,y))
12:		OR(x,y)	→ AND(x,y)
13:		OR(x,y)	→ XOR(x,y)
14:		IMPLIES(x,y)	→ XOR(and(x,y),xor(x,true))
15:		IMPLIES(x,y)	→ AND(x,y)
16:		IMPLIES(x,y)	→ XOR(x,true)
17:		AND(xor(x,y),z)	→ XOR(and(x,z),and(y,z))
18:		AND(xor(x,y),z)	→ AND(x,z)
19:		AND(xor(x,y),z)	→ AND(y,z)

The approximated dependency graph contains one SCC: {18,19}.

Consider the SCC {18,19}. There are no usable rules. By taking the AF π with π(AND) = 1 together with the lexicographic path order with empty precedence, the rules in {18,19} are strictly decreasing.

Hence the TRS is terminating.

Tyrolean Termination Tool (0.01 seconds) --- May 4, 2006